Inference at * 
Iof proof for Lemma not-not-assert:


  b:. ((b))  (b) 

latex

 by (Auto) 
CollapseTHEN ((Try ((D (0)) 
CollapseTHEN ((Complete (Auto)))))) 

latex

C1: 

C1: 1. b : 
C1: 2. (b)
C1:   b
C.

Definitions	P  Q, P & Q, P  Q, Void, , , Type, if b then t else f fi , True, case b of inl(x) => s(x) | inr(y) => t(y), x:AB(x), P  Q, False, A, b, x:A. B(x), t  T
Lemmas	bool wf, not wf, assert wf